SESAxioms{i:l}(E;T;pred?;info;when;after;time)
== (e:E, l:IdLnk.
== (e':E
== ((e'':E.
== ((rcv?(e''))
== ( (sender(e'') = e)
== ( (link(e'') = l)
== ( (((e'' = e')  e'' < e') & loc(e') = destination(l))))
== & (((e, e':E. (loc(e) = loc(e'))  (pred?(e) = pred?(e'))  (e = e'))
== & (& SWellFounded(pred!(e;e'))
== & (& (e:E. ((first(e)))  (loc(pred(e)) = loc(e)))
== & (& (e:E. (rcv?(e))  (loc(sender(e)) = source(link(e))))
== & (& (e, e':E.
== & (& ((rcv?(e))  (rcv?(e'))  (link(e) = link(e'))  sender(e) < sender(e')  e < e'))
== & (c (e:E.
== & (c ((first(e)))
== & (c  (x:Id, t:. when(x,e,t) = after(x,pred(e),t + ((time(e)) - (time(pred(e)))))))) 

latex

---

clarification:

SESAxioms{i:l}
SESAxioms(E; T; pred?; info; when; after; time)
== (e:E, l:IdLnk.
== (e':E
== ((e'':E.
== ((rcv?(info;e''))
== ( (sender(info;e'') = e  E)
== ( (link(info;e'') = l  IdLnk)
== ( (((e'' = e'  E)  cless(E;pred?;info;e'';e')) & loc(info;e') = destination(l)  Id)))
== & (((e:E, e':E.
== & ((((loc(info;e) = loc(info;e')  Id)  (pred?(e) = pred?(e')  (E + Unit))  (e = e'  E))
== & (& strongwellfounded(E; e,e'.pred!(E;pred?;info;e;e'))
== & (& (e:E. ((first(pred?;e)))  (loc(info;pred(pred?;e)) = loc(info;e)  Id))
== & (& (e:E. (rcv?(info;e))  (loc(info;sender(info;e)) = source(link(info;e))  Id))
== & (& (e:E, e':E.
== & (& ((rcv?(info;e))
== & (& ( (rcv?(info;e'))
== & (& ( (link(info;e) = link(info;e')  IdLnk)
== & (& ( cless(E;pred?;info;sender(info;e);sender(info;e'))
== & (& ( cless(E;pred?;info;e;e')))
== & (c (e:E.
== & (c ((first(pred?;e)))
== & (c  (x:Id, t:.
== & (c  when(x,e,t)
== & (c  =
== & (c  after(x,pred(pred?;e),t + ((time(e)) - (time(pred(pred?;e)))))
== & (c   T(loc(info;e),x)))) 

latex

Definitions	x:A. B(x), P  Q, destination(l), A c B, left + right, Unit, SWellFounded(R(x;y)), pred!(e;e'), P & Q, source(l), rcv?(e), IdLnk, link(e), sender(e), e < e', P  Q, A, b, first(e), Id, x:A. B(x), s = t, loc(e), f(a), pred(e)
FDL editor aliases	SESAxioms